#include <signal.h>
#include "sat_parse.h"
#include <synit.h>
#include "cktsat/cktcover.h"
#include "cryptominisat/Main.h"
#include "cktsat/csatsolver.h"
#include <fstream>

void runtime(const char * s )
{
   static clock_t sclk = clock(), oclk = clock();
   clock_t clk = clock();
   cout << "c " << s << " " << (1.0*(clk-oclk)/CLOCKS_PER_SEC) << " total " << (1.0*(clk-sclk)/CLOCKS_PER_SEC) << endl;
   oclk = clk;
}
void mySIGINT_handler( int )
{
   runtime( "interrupt " );
   cout << "c INTERRUPTED ... "<<endl;
   cout << "s UNKNOWN" <<endl;
   exit(1);
}
static void movefile( const char * src , const char * des)
{
   std::ifstream ifs(src, std::ios::binary);
   std::ofstream ofs(des, std::ios::binary);
   ofs << ifs.rdbuf();
}
static void optimize( InfoCut & in , CktCover & out )
{
   unsigned osize , nsize;

   InfoCut * current = & in;
   InfoCut * next = new InfoCut;

   do
   {
      current->init();
      synit( *current , *next );
      osize = current->size();
      nsize = next->size();

      if( current != & in )delete current;
      if( (1.0*(nsize+1)/(osize+1)) > 0.8 )break;

      current = next ;
      next = new InfoCut;
   }while(1);
   next->init();
   next->factor( out );
   delete next;
}
static void dump_solution( CryptoMiniSat::Solver & S , lit_t * l , StrashAIG & ckt , vector<AigIndex> & link )
{
   uint8_t * solution = new uint8_t [ckt.sz];
   solution[0] = 0;
   uint32_t v0 = l[0].var();
   for( unsigned i = 1 ; i < ckt._andFlag ; ++ i )
   {
      if( l[i].var() == v0 ) solution[i] = l[i].sign()?0:1; 
      else solution[i] = S.modelValue( l[i] ) == CryptoMiniSat::l_True ? 1 : 0;
   }
   for( unsigned i = ckt._andFlag ; i < ckt.sz ; ++ i )
   {
      AigNode n = ckt.data[i];
      solution[i] = (sign(n.fanin[0]) ^ solution[ var( n.fanin[0] ) ]) & (sign(n.fanin[1]) ^ solution[ var( n.fanin[1] )] ) & 1 ;
   }
   cout << "v ";
   for( int i = 1 ; i < (int)link.size() ; ++ i ) // int because of -i use in the code
   {
      QuteRSAT::AigIndex x = link[i];

      if ( x._data == UINT_MAX) 
         cout << i << " ";
      else
         cout << ((solution[x._index]^x._sign)?-i:i) << " " ;
   }
   cout << "0" << endl;
   delete [] solution;
}
int main( int argc , const char ** argv )
{
   vector<AigIndex> link;
   InfoCut  opt;
   CktCover ckt;
   CryptoMiniSat::lbool    sat;
   double cover_rate;

   bool nopt = false;

   signal(SIGALRM, mySIGINT_handler);
   signal(SIGINT, mySIGINT_handler);
   signal(SIGTERM, mySIGINT_handler);
   runtime( "start ");

   {
      AigCircuit rckt;
      gzFile f = (argc == 1) ? gzdopen(0, "rb") : gzopen( argv[1], "rb");
      StreamBuffer in(f);

      unsigned nvar = parse_header( in ); 
      CnfToAig tran( nvar+1 , rckt, link );
      parse_DIMACS( in , tran );
      gzclose( f );

      tran.run(); 
      if( tran.isUnSat() ) 
      {
         runtime( "solve time ");
         cout << "s UNSATISFIABLE" <<endl;
         return 0;
      }
      cover_rate = tran.getCoverRate();
      cout << "c cover rate " << cover_rate << endl;
      

      runtime( "rocky end ");
      nopt = (rckt.size() < 200000) || ( cover_rate < 50 ) ;
      if( ! nopt ) 
      {
         rckt.transform( opt , link );
         optimize( opt , ckt );
         cout << "c circuit size reduce "  << opt.size() << " " << ckt.size() << endl;
         runtime( "opt time ");
      }else
      {
         rckt.transform( ckt , link );
      }
   }
   ckt.init( true );
   ckt.covering();
   ckt.assignLit();
   runtime( "covering time ");
   
   CryptoMiniSat::SolverConf solconf; 
   solconf.libraryUsage = false;
   if( argc == 3 ) solconf.origSeed = atoi( argv[2] ); 
   CryptominisatSolver S(solconf);

   unsigned vs = ckt.nVars();
   for( unsigned i = 0 ; i < vs ; ++i ) S.newVar();

   ckt.const_propagation( );
   //ckt.assignCNFPO( S ); // 2 select 1 const propagation or assign po 
   ckt.assignCNF( S );
   sat = S.solve();
  
   runtime( "solve time ");
   if( sat == CryptoMiniSat::l_True )
   {
      cout << "s SATISFIABLE "<< endl;
      dump_solution( S , ckt._lits , nopt ? ckt : opt , link );
   }
   else if( sat == CryptoMiniSat::l_False )
      cout << "s UNSATISFIABLE "<< endl;
   else 
      cout << "s UNKNOWN" <<endl;
}
/*if( cover_rate < 50 )
      {
         string randstr = "--randomize=" ;
         const char * nargv[4] = {argv[0],argv[1]};
         if( argc == 3 )
         { 
            randstr = randstr + string(argv[2]) ;
            nargv[1]= randstr.c_str();
            nargv[2] = argv[1]; 
         }
         Main main( argc , nargv);
         main.parseCommandLine();
         return main.singleThreadSolve();
      }*/

